{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes       #-}
{-# LANGUAGE Rank2Types        #-}
{-# LANGUAGE TemplateHaskell   #-}
{-# LANGUAGE TypeFamilies      #-}
{-# LANGUAGE ViewPatterns      #-}
{-# LANGUAGE DeriveGeneric     #-}
{-# LANGUAGE DeriveAnyClass    #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

{- |
Module      :  Types.hs
Description :  Central data type and Yesod typeclass instances.
Copyright   :  (c) 2011 Cedric Staub
License     :  GPL-3

Maintainer  :  Simon Meier <iridcode@gmail.com>
Stability   :  experimental
Portability :  non-portable
-}


module Web.Types
  ( WebUI(..)
  , Route (..)
  , resourcesWebUI
  , TheoryInfo(..)
  , DiffTheoryInfo(..)
  , EitherTheoryInfo(..)
  , isTheoryInfo
  , isDiffTheoryInfo
  , getEitherTheoryName
  , getEitherTheoryTime
  , getEitherTheoryPrimary
  , getEitherTheoryOrigin
  , getEitherTheoryIndex
  , TheoryPath(..)
  , DiffTheoryPath(..)
  , TheoryOrigin(..)
  , JsonResponse(..)
  , TheoryIdx
  , TheoryMap
  , ThreadMap
  -- , GenericHandler
  , Handler
  -- , URL rendering function
  , RenderUrl
  -- , GenericWidget
  , Widget
  -- Image rendering
  , ImageFormat(..)
  , imageFormatMIME
  )
where


-- import           Control.Applicative
import           Control.Concurrent
import           Data.Label
import qualified Data.Map            as M
import           Data.Maybe          (listToMaybe)
-- import           Data.Monoid         (mconcat)
import           Data.Ord            (comparing)
import qualified Data.Text           as T
import           Data.Time.LocalTime
import qualified Data.Binary         as Bin
import           Data.Binary.Orphans()
import           Data.Binary.Instances()

import           Control.DeepSeq
import           GHC.Generics (Generic)

import           Text.Hamlet
import           Yesod.Core
import           Yesod.Static

import           Theory
import Control.Monad.Except (ExceptT)
import Main.TheoryLoader
import Theory.Tools.Wellformedness (WfErrorReport)


------------------------------------------------------------------------------
-- Types
------------------------------------------------------------------------------

-- | Type synonym for a generic handler inside our site.
-- type GenericHandler m = Handler WebUI WebUI m
-- type Handler a = Handler WebUI WebUI a

-- | Type synonym for a generic widget inside our site.
-- type GenericWidget m = Widget WebUI (GenericHandler m)
-- type Widget a = Widget WebUI WebUI a

-- | Type synonym representing a numeric index for a theory.
type TheoryIdx = Int

-- | Type synonym representing a map of theories.
type TheoryMap = M.Map TheoryIdx (EitherTheoryInfo)

-- | Type synonym representing a map of threads.
type ThreadMap = M.Map T.Text ThreadId

-- | The image format used for rendering graphs.
data ImageFormat = PNG | SVG

instance Show ImageFormat where
    show PNG = "png"
    show SVG = "svg"

-- | convert image format to MIME type.
imageFormatMIME :: ImageFormat -> String
imageFormatMIME PNG = "image/png"
imageFormatMIME SVG = "image/svg+xml"

-- | The so-called site argument for our application, which can hold various
-- information that can use to keep info that needs to be available to the
-- handler functions.
data WebUI = WebUI
  { getStatic          :: Static
    -- ^ Settings for static file serving.
  , cacheDir           :: FilePath
    -- ^ The caching directory (for storing rendered graphs).
  , workDir            :: FilePath
    -- ^ The working directory (for storing/loading theories).
  , thyOpts            :: TheoryLoadOptions
    -- ^ Options for loading theories
  , loadThy            :: String -> FilePath -> ExceptT TheoryLoadError IO (Either OpenTheory OpenDiffTheory)
    -- ^ Load a theory according to command-line arguments.
  , closeThy           :: SignatureWithMaude -> Either OpenTheory OpenDiffTheory -> ExceptT TheoryLoadError IO (WfErrorReport, Either ClosedTheory ClosedDiffTheory)
    -- ^ Close an open theory according to command-line arguments.
  , theoryVar          :: MVar (TheoryMap)
    -- ^ MVar that holds the theory map
  , threadVar          :: MVar ThreadMap
    -- ^ MVar that holds the thread map
  , autosaveProofstate :: Bool
    -- ^ Automatically store theory map
  , graphCmd           :: (String, FilePath)
    -- ^ The dot or json command with additional flag to indicate choice dot, json, ...
  , imageFormat        :: ImageFormat
    -- ^ The image-format used for rendering graphs
  , defaultAutoProver  :: AutoProver
    -- ^ The default prover to use for automatic proving.
  , debug              :: Bool
    -- ^ Output debug messages
  }


-- | Simple data type for generating JSON responses.
data JsonResponse
  = JsonHtml T.Text Content   -- ^ Title and HTML content
  | JsonAlert T.Text          -- ^ Alert/dialog box with message
  | JsonRedirect T.Text       -- ^ Redirect to given URL

-- | Data type representing origin of theory.
-- Command line with file path, upload with filename (not path),
-- or created by interactive mode (e.g. through editing).
data TheoryOrigin = Local FilePath | Upload String | Interactive
     deriving (Show, Eq, Ord, Generic, Bin.Binary, NFData)

-- | Data type containg both the theory and it's index, making it easier to
-- pass the two around (since they are always tied to each other). We also
-- keep some extra bookkeeping information.
data TheoryInfo = TheoryInfo
  { tiIndex      :: TheoryIdx       -- ^ Index of theory.
  , tiTheory     :: ClosedTheory    -- ^ The closed theory.
  , tiTime       :: ZonedTime       -- ^ Time theory was loaded.
  , tiParent     :: Maybe TheoryIdx -- ^ Prev theory in history
  , tiPrimary    :: Bool            -- ^ This is the orginally loaded theory.
  , tiOrigin     :: TheoryOrigin    -- ^ Origin of theory.
  , tiAutoProver :: AutoProver      -- ^ The automatic prover to use.
  , tiErrorsHtml :: String
  } deriving (Generic, Bin.Binary)

-- | Data type containg both the theory and it's index, making it easier to
-- pass the two around (since they are always tied to each other). We also
-- keep some extra bookkeeping information.
data DiffTheoryInfo = DiffTheoryInfo
  { dtiIndex      :: TheoryIdx       -- ^ Index of theory.
  , dtiTheory     :: ClosedDiffTheory -- ^ The closed theory.
  , dtiTime       :: ZonedTime       -- ^ Time theory was loaded.
  , dtiParent     :: Maybe TheoryIdx -- ^ Prev theory in history
  , dtiPrimary    :: Bool            -- ^ This is the orginally loaded theory.
  , dtiOrigin     :: TheoryOrigin    -- ^ Origin of theory.
  , dtiAutoProver :: AutoProver      -- ^ The automatic prover to use.
  , dtiErrorsHtml :: String
  } deriving (Generic, Bin.Binary)


-- | We use the ordering in order to display loaded theories to the user.
-- We first compare by name, then by time loaded, and then by source: Theories
-- that were loaded from the command-line are displayed earlier then
-- interactively loaded ones.
compareTI :: TheoryInfo -> TheoryInfo -> Ordering
compareTI (TheoryInfo _ i1 t1 p1 a1 o1 _ _) (TheoryInfo _ i2 t2 p2 a2 o2 _ _) =
  mconcat
    [ comparing (get thyName) i1 i2
    , comparing zonedTimeToUTC t1 t2
    , compare a1 a2
    , compare p1 p2
    , compare o1 o2
    ]

-- | We use the ordering in order to display loaded theories to the user.
-- We first compare by name, then by time loaded, and then by source: Theories
-- that were loaded from the command-line are displayed earlier then
-- interactively loaded ones.
compareDTI :: DiffTheoryInfo -> DiffTheoryInfo -> Ordering
compareDTI (DiffTheoryInfo _ i1 t1 p1 a1 o1 _ _) (DiffTheoryInfo _ i2 t2 p2 a2 o2 _ _) =
  mconcat
    [ comparing (get diffThyName) i1 i2
    , comparing zonedTimeToUTC t1 t2
    , compare a1 a2
    , compare p1 p2
    , compare o1 o2
    ]

data EitherTheoryInfo = Trace TheoryInfo | Diff DiffTheoryInfo deriving (Generic, Bin.Binary)

-- instance Bin.Binary TheoryInfo
-- instance Bin.Binary DiffTheoryInfo
-- instance Bin.Binary EitherTheoryInfo

{- instance Bin.Binary EitherTheoryInfo where
       put (Trace i) = do Bin.put (0 :: Bin.Word8)
                            Bin.put i
       put (Diff i)    = do Bin.put (1 :: Bin.Word8)
       Bin.put i -}
{-       get = do t <- get :: Bin.Get Bin.Word8
                case t of
                           0 -> do i <- Bin.get
                                   return (Trace i)
                           1 -> do i <- Bin.get
                           return (Diff i) -}
{-       get = do tag <- Bin.getWord8
                case tag of
                    0 -> liftM Trace get
                    1 -> liftM Diff get -}

-- Direct access functionf for Either Theory Type
getEitherTheoryName :: EitherTheoryInfo -> String
getEitherTheoryName (Trace i)  = get thyName (tiTheory i)
getEitherTheoryName (Diff i) = get diffThyName (dtiTheory i)

isTheoryInfo :: EitherTheoryInfo -> Bool
isTheoryInfo (Trace _) = True
isTheoryInfo (Diff  _) = False

isDiffTheoryInfo :: EitherTheoryInfo -> Bool
isDiffTheoryInfo (Trace _) = False
isDiffTheoryInfo (Diff  _) = True

getEitherTheoryTime :: EitherTheoryInfo -> ZonedTime
getEitherTheoryTime (Trace i)  = (tiTime i)
getEitherTheoryTime (Diff i) = (dtiTime i)

getEitherTheoryPrimary :: EitherTheoryInfo -> Bool
getEitherTheoryPrimary (Trace i)  = (tiPrimary i)
getEitherTheoryPrimary (Diff i) = (dtiPrimary i)

getEitherTheoryOrigin :: EitherTheoryInfo -> TheoryOrigin
getEitherTheoryOrigin (Trace i)  = (tiOrigin i)
getEitherTheoryOrigin (Diff i) = (dtiOrigin i)

getEitherTheoryIndex :: EitherTheoryInfo -> TheoryIdx
getEitherTheoryIndex (Trace i)  = (tiIndex i)
getEitherTheoryIndex (Diff i) = (dtiIndex i)

-- | We use the ordering in order to display loaded theories to the user.
-- We first compare by name, then by time loaded, and then by source: Theories
-- that were loaded from the command-line are displayed earlier then
-- interactively loaded ones.
compareEDTI :: EitherTheoryInfo -> EitherTheoryInfo -> Ordering
compareEDTI (Trace (TheoryInfo _ i1 t1 p1 a1 o1 _ _)) (Trace (TheoryInfo _ i2 t2 p2 a2 o2 _ _)) =
  mconcat
    [ comparing (get thyName) i1 i2
    , comparing zonedTimeToUTC t1 t2
    , compare a1 a2
    , compare p1 p2
    , compare o1 o2
    ]
compareEDTI (Diff (DiffTheoryInfo _ i1 t1 p1 a1 o1 _ _)) (Diff (DiffTheoryInfo _ i2 t2 p2 a2 o2 _ _)) =
  mconcat
    [ comparing (get diffThyName) i1 i2
    , comparing zonedTimeToUTC t1 t2
    , compare a1 a2
    , compare p1 p2
    , compare o1 o2
    ]
compareEDTI (Diff (DiffTheoryInfo _ i1 t1 p1 a1 o1 _ _)) (Trace (TheoryInfo _ i2 t2 p2 a2 o2 _ _)) =
  mconcat
    [ compare ((get diffThyName) i1) ((get thyName) i2)
    , comparing zonedTimeToUTC t1 t2
    , compare a1 a2
    , compare p1 p2
    , compare o1 o2
    ]
compareEDTI (Trace (TheoryInfo _ i1 t1 p1 a1 o1 _ _)) (Diff (DiffTheoryInfo _ i2 t2 p2 a2 o2 _ _)) =
  mconcat
    [ compare ((get thyName) i1) ((get diffThyName) i2)
    , comparing zonedTimeToUTC t1 t2
    , compare a1 a2
    , compare p1 p2
    , compare o1 o2
    ]


instance Eq (TheoryInfo) where
  (==) t1 t2 = compareTI t1 t2 == EQ

instance Ord (TheoryInfo) where
  compare = compareTI

instance Eq (DiffTheoryInfo) where
  (==) t1 t2 = compareDTI t1 t2 == EQ

instance Ord (DiffTheoryInfo) where
  compare = compareDTI


instance Eq (EitherTheoryInfo) where
  (==) t1 t2 = compareEDTI t1 t2 == EQ

instance Ord (EitherTheoryInfo) where
  compare = compareEDTI

-- | Simple data type for specifying a path to a specific
-- item within a theory.
data TheoryPath
  = TheoryHelp                          -- ^ The help view (help and info about theory)
  | TheoryLemma String                  -- ^ Theory lemma with given name
  | TheorySource SourceKind Int Int     -- ^ Required cases (i'th source, j'th case)
  | TheoryProof String ProofPath        -- ^ Proof path within proof for given lemma
  | TheoryMethod String ProofPath Int   -- ^ Apply the proof method to proof path
  | TheoryRules                         -- ^ Theory rules
  | TheoryMessage                       -- ^ Theory message deduction
  | TheoryTactic                        -- ^ Theory tactic
  deriving (Eq, Show, Read)

-- | Simple data type for specifying a path to a specific
-- item within a theory.
data DiffTheoryPath
  = DiffTheoryHelp                                    -- ^ The help view (help and info about theory)
  | DiffTheoryLemma Side String                       -- ^ Theory lemma with given name and side
  | DiffTheoryDiffLemma String                        -- ^ Theory DiffLemma with given name
  | DiffTheorySource Side SourceKind Bool Int Int     -- ^ Required cases (i'th source, j'th case)
  | DiffTheoryProof Side String ProofPath             -- ^ Proof path within proof for given lemma
  | DiffTheoryDiffProof String ProofPath              -- ^ Proof path within proof for given lemma
  | DiffTheoryMethod Side String ProofPath Int        -- ^ Apply the proof method to proof path
  | DiffTheoryDiffMethod String ProofPath Int         -- ^ Apply the proof method to proof path
  | DiffTheoryRules Side Bool                         -- ^ Theory rules per side
  | DiffTheoryDiffRules                               -- ^ Theory rules unprocessed
  | DiffTheoryMessage Side Bool                       -- ^ Theory message deduction per side
  deriving (Eq, Show, Read)

-- | Render a theory path to a list of strings. Note that we prefix an
-- underscore to the empty string and strings starting with an underscore.
-- This avoids empty path segments, which seem to trip up certain versions of
-- Yesod.
renderTheoryPath :: TheoryPath -> [String]
renderTheoryPath =
    map prefixWithUnderscore . go
  where
    go TheoryHelp = ["help"]
    go TheoryRules = ["rules"]
    go TheoryMessage = ["message"]
    go (TheoryLemma name) = ["lemma", name]
    go (TheorySource k i j) = ["cases", show k, show i, show j]
    go (TheoryProof lemma path) = "proof" : lemma : path
    go (TheoryMethod lemma path idx) = "method" : lemma : show idx : path
    go TheoryTactic = ["tactic"]

-- | Render a theory path to a list of strings. Note that we prefix an
-- underscore to the empty string and strings starting with an underscore.
-- This avoids empty path segments, which seem to trip up certain versions of
-- Yesod.
renderDiffTheoryPath :: DiffTheoryPath -> [String]
renderDiffTheoryPath =
    map prefixWithUnderscore . go
  where
    go DiffTheoryHelp = ["help"]
    go (DiffTheoryLemma s name) = ["lemma", show s, name]
    go (DiffTheoryDiffLemma name) = ["difflemma", name]
    go (DiffTheorySource s k i j d) = ["cases", show s, show k, show i, show j, show d]
    go (DiffTheoryProof s lemma path) = "proof" : show s : lemma : path
    go (DiffTheoryDiffProof lemma path) = "diffProof" : lemma : path
    go (DiffTheoryMethod s lemma path idx) = "method" : show s : lemma : show idx : path
    go (DiffTheoryDiffMethod lemma path idx) = "diffMethod" : lemma : show idx : path
    go (DiffTheoryRules s d) = ["rules", show s, show d]
    go (DiffTheoryDiffRules) = ["diffrules"]
    go (DiffTheoryMessage s d) = ["message", show s, show d]

-- | Prefix an underscore to the empty string and strings starting with an
-- underscore.
prefixWithUnderscore :: String -> String
prefixWithUnderscore ""         = "_"
prefixWithUnderscore cs@('_':_) = '_' : cs
prefixWithUnderscore cs         = cs

-- | Remove an underscore prefix. It holds that
--
-- > unprefixUnderscore . prefixWithUnderscore = id
--
-- The inverted composition holds for all strings except the empty string and
-- strings starting with an underscore.
unprefixUnderscore :: String -> String
unprefixUnderscore "_"              = ""
unprefixUnderscore ('_':cs@('_':_)) = cs
unprefixUnderscore cs               = cs

-- | Parse a list of strings into a theory path.
parseTheoryPath :: [String] -> Maybe TheoryPath
parseTheoryPath =
    parse . map unprefixUnderscore
  where
    parse []     = Nothing
    parse (x:xs) = case x of
      "help"    -> Just TheoryHelp
      "rules"   -> Just TheoryRules
      "message" -> Just TheoryMessage
      "tactic"  -> Just TheoryTactic
      "lemma"   -> parseLemma xs
      "cases"   -> parseCases xs
      "proof"   -> parseProof xs
      "method"  -> parseMethod xs
      _         -> Nothing

    safeRead = listToMaybe . map fst . reads

    parseLemma ys = TheoryLemma <$> listToMaybe ys

    parseProof (y:ys) = Just (TheoryProof y ys)
    parseProof _      = Nothing

    parseMethod (y:z:zs) = safeRead z >>= Just . TheoryMethod y zs
    parseMethod _        = Nothing

    parseCases (kind:y:z:_) = do
      k <- case kind of "refined" -> return RefinedSource
                        "raw"     -> return RawSource
                        _         -> Nothing
      m <- safeRead y
      n <- safeRead z
      return (TheorySource k m n)
    parseCases _       = Nothing

-- | Parse a list of strings into a theory path.
parseDiffTheoryPath :: [String] -> Maybe DiffTheoryPath
parseDiffTheoryPath =
    parse . map unprefixUnderscore
  where
    parse []     = Nothing
    parse (x:xs) = case x of
      "help"      -> Just DiffTheoryHelp
      "diffrules" -> Just DiffTheoryDiffRules
      "rules"     -> parseRules xs
      "message"   -> parseMessage xs
      "lemma"     -> parseLemma xs
      "difflemma" -> parseDiffLemma xs
      "cases"     -> parseCases xs
      "proof"     -> parseProof xs
      "diffProof" -> parseDiffProof xs
      "method"    -> parseMethod xs
      "diffMethod"-> parseDiffMethod xs
      _           -> Nothing

    safeRead :: Read a => String -> Maybe a
    safeRead  = listToMaybe . map fst . reads

    parseRules :: [String] -> Maybe DiffTheoryPath
    parseRules (y:z:_) = do
      s <- case y of "LHS" -> return LHS
                     "RHS" -> return RHS
                     _     -> Nothing
      d <- case z of "True"  -> return True
                     "False" -> return False
                     _       -> Nothing
      return (DiffTheoryRules s d)
    parseRules _         = Nothing

    parseMessage :: [String] -> Maybe DiffTheoryPath
    parseMessage (y:z:_) = do
      s <- case y of "LHS" -> return LHS
                     "RHS" -> return RHS
                     _     -> Nothing
      d <- case z of "True"  -> return True
                     "False" -> return False
                     _       -> Nothing
      return (DiffTheoryMessage s d)
    parseMessage _         = Nothing

    parseLemma :: [String] -> Maybe DiffTheoryPath
    parseLemma (y:ys) = do
      s <- case y of "LHS" -> return LHS
                     "RHS" -> return RHS
                     _     -> Nothing
      return (DiffTheoryLemma s (head ys))
    parseLemma _         = Nothing

    parseDiffLemma :: [String] -> Maybe DiffTheoryPath
    parseDiffLemma ys = DiffTheoryDiffLemma <$> listToMaybe ys

    parseProof :: [String] -> Maybe DiffTheoryPath
    parseProof (y:z:zs) = do
      s <- case y of "LHS" -> return LHS
                     "RHS" -> return RHS
                     _     -> Nothing
      return (DiffTheoryProof s z zs)
    parseProof _         = Nothing

    parseDiffProof :: [String] -> Maybe DiffTheoryPath
    parseDiffProof (z:zs) = do
      return (DiffTheoryDiffProof z zs)
    parseDiffProof _         = Nothing

    parseMethod :: [String] -> Maybe DiffTheoryPath
    parseMethod (x:y:z:zs) = do
      s <- case x of "LHS" -> return LHS
                     "RHS" -> return RHS
                     _     -> Nothing
      i <- safeRead z
      return (DiffTheoryMethod s y zs i)
    parseMethod _        = Nothing

    parseDiffMethod :: [String] -> Maybe DiffTheoryPath
    parseDiffMethod (y:z:zs) = do
      i <- safeRead z
      return (DiffTheoryDiffMethod y zs i)
    parseDiffMethod _        = Nothing

    parseCases :: [String] -> Maybe DiffTheoryPath
    parseCases (x:kind:pd:y:z:_) = do
      s <- case x of "LHS" -> return LHS
                     "RHS" -> return RHS
                     _     -> Nothing
      k <- case kind of "refined" -> return RefinedSource
                        "raw"     -> return RawSource
                        _         -> Nothing
      d <- case pd of "True"  -> return True
                      "False" -> return False
                      _       -> Nothing
      m <- safeRead y
      n <- safeRead z
      return (DiffTheorySource s k d m n)
    parseCases _       = Nothing

type RenderUrl = Route (WebUI) -> T.Text

------------------------------------------------------------------------------
-- Routing
------------------------------------------------------------------------------

-- | Static routing for our application.
-- Note that handlers ending in R are general handlers,
-- whereas handlers ending in MR are for the main view
-- and the ones ending in DR are for the debug view.
mkYesodData "WebUI" [parseRoutes|
/                                          RootR                   GET POST
/thy/trace/#Int/overview/*TheoryPath          OverviewR               GET
/thy/trace/#Int/source                           TheorySourceR           GET
/thy/trace/#Int/message                          TheoryMessageDeductionR GET
/thy/trace/#Int/main/*TheoryPath              TheoryPathMR            GET
-- /thy/trace/#Int/debug/*TheoryPath             TheoryPathDR            GET
/thy/trace/#Int/graph/*TheoryPath             TheoryGraphR            GET
/thy/trace/#Int/autoprove/#SolutionExtractor/#Int/*TheoryPath AutoProverR             GET
/thy/trace/#Int/autoproveAll/#SolutionExtractor/#Int/*TheoryPath AutoProverAllR             GET
/thy/trace/#Int/next/#String/*TheoryPath      NextTheoryPathR         GET
/thy/trace/#Int/prev/#String/*TheoryPath      PrevTheoryPathR         GET
-- /thy/trace/#Int/save                             SaveTheoryR             GET
/thy/trace/#Int/download/#String                 DownloadTheoryR         GET
-- /thy/trace/#Int/edit/source                      EditTheoryR             GET POST
-- /thy/trace/#Int/edit/path/*TheoryPath         EditPathR               GET POST
/thy/trace/#Int/del/path/*TheoryPath          DeleteStepR             GET
/thy/trace/#Int/unload                           UnloadTheoryR           GET
/thy/equiv/#Int/overview/*DiffTheoryPath      OverviewDiffR               GET
/thy/equiv/#Int/source                           TheorySourceDiffR           GET
/thy/equiv/#Int/message                          TheoryMessageDeductionDiffR GET
/thy/equiv/#Int/main/*DiffTheoryPath          TheoryPathDiffMR            GET
-- /thy/equiv/#Int/debug/*DiffTheoryPath             TheoryPathDiffDR            GET
/thy/equiv/#Int/graph/*DiffTheoryPath         TheoryGraphDiffR            GET
/thy/equiv/#Int/mirror/*DiffTheoryPath        TheoryMirrorDiffR            GET
/thy/equiv/#Int/autoprove/#SolutionExtractor/#Int/#Side/*DiffTheoryPath AutoProverDiffR             GET
/thy/equiv/#Int/autoproveAll/#SolutionExtractor/#Int AutoProverAllDiffR             GET
/thy/equiv/#Int/autoproveDiff/#SolutionExtractor/#Int/*DiffTheoryPath AutoDiffProverR             GET
/thy/equiv/#Int/next/#String/*DiffTheoryPath  NextTheoryPathDiffR         GET
/thy/equiv/#Int/prev/#String/*DiffTheoryPath  PrevTheoryPathDiffR         GET
-- /thy/equiv/#Int/save                             SaveTheoryR             GET
/thy/equiv/#Int/download/#String                 DownloadTheoryDiffR         GET
-- /thy/equiv/#Int/edit/source                      EditTheoryR             GET POST
-- /thy/equiv/#Int/edit/path/*DiffTheoryPath         EditPathDiffR               GET POST
/thy/equiv/#Int/del/path/*DiffTheoryPath      DeleteStepDiffR             GET
/thy/equiv/#Int/unload                           UnloadTheoryDiffR           GET
/kill                                      KillThreadR             GET
-- /threads                                   ThreadsR                GET
/robots.txt                                RobotsR                 GET
/favicon.ico                               FaviconR                GET
/static                                    StaticR                 Static getStatic
|]


instance PathPiece SolutionExtractor where
  toPathPiece CutNothing         = "characterize"
  toPathPiece CutDFS             = "idfs"
  toPathPiece CutBFS             = "bfs"
  toPathPiece CutSingleThreadDFS = "seqdfs"

  fromPathPiece "characterize" = Just CutNothing
  fromPathPiece "idfs"         = Just CutDFS
  fromPathPiece "bfs"          = Just CutBFS
  fromPathPiece "seqdfs"       = Just CutSingleThreadDFS
  fromPathPiece _              = Nothing

instance PathPiece Side where
  toPathPiece LHS = "LHS"
  toPathPiece RHS = "RHS"

  fromPathPiece "LHS" = Just LHS
  fromPathPiece "RHS" = Just RHS
  fromPathPiece _     = Nothing


-- | MultiPiece instance for TheoryPath.
instance PathMultiPiece TheoryPath where
  toPathMultiPiece   = map T.pack . renderTheoryPath
  fromPathMultiPiece = parseTheoryPath . map T.unpack

-- | MultiPiece instance for DiffTheoryPath.
instance PathMultiPiece DiffTheoryPath where
  toPathMultiPiece   = map T.pack . renderDiffTheoryPath
  fromPathMultiPiece = parseDiffTheoryPath . map T.unpack

-- Instance of the Yesod typeclass.
instance Yesod WebUI where
  -- | The approot. We can leave this empty because the
  -- application is always served from the root of the server.
  approot = ApprootStatic T.empty

  -- | The default layout for rendering.
  defaultLayout = defaultLayout'

  -- | The path cleaning function. We make sure empty strings
  -- are not scrubbed from the end of the list. The default
  -- cleanPath function forces canonical URLs.
  cleanPath _ = Right

------------------------------------------------------------------------------
-- Default layout
------------------------------------------------------------------------------

-- | Our application's default layout template.
-- Note: We define the default layout here even tough it doesn't really
-- belong in the "types" module in order to avoid mutually recursive modules.
-- defaultLayout' :: (Yesod master, Route master ~ WebUIRoute)
--                => Widget master ()      -- ^ Widget to embed in layout
--                -> Handler master Html
defaultLayout' :: Widget -> Handler Html
defaultLayout' w = do
  page <- widgetToPageContent w
  message <- getMessage
  withUrlRenderer [hamlet|
    $newline never
    !!!
    <html>
      <head>
        <title>#{pageTitle page}
        <link rel=stylesheet href=/static/css/tamarin-prover-ui.css>
        <link rel=stylesheet href=/static/css/jquery-contextmenu.css>
        <link rel=stylesheet href=/static/css/smoothness/jquery-ui.css>
        <script src=/static/js/jquery.js></script>
        <script src=/static/js/jquery-ui.js></script>
        <script src=/static/js/jquery-layout.js></script>
        <script src=/static/js/jquery-cookie.js></script>
        <script src=/static/js/jquery-superfish.js></script>
        <script src=/static/js/jquery-contextmenu.js></script>
        <script src=/static/js/tamarin-prover-ui.js></script>
        ^{pageHead page}
      <body>
        $maybe msg <- message
          <p.message>#{msg}
        <p.loading>
          Loading, please wait...
          \  <a id=cancel href='#'>Cancel</a>
        ^{pageBody page}
        <div#dialog>
        <ul#contextMenu>
          <li.autoprove>
            <a href="#autoprove">Autoprove</a>
  |]
          -- <li.delstep>
            -- <a href="#del/path">Remove step</a>

